@i x has type T == e@i. (x when e)  T & (x after e)  T 

latex

---

clarification:

es-type(es; i; x; T) == alle-at(es;i;e.es-when(es; x; e)  T & es-after(es; x; e)  T) 

latex

Definitions	e@i. P(e), P & Q, x when e, t  T, (x after e)
FDL editor aliases	es-type